Nuprl Lemma : rfunction_void_wf
12,41
postcript
pdf
{
f
|
x
:Void
Void}
Type
latex
ProofTree
Definitions
t
T
,
{
T
}
,
x
(
s
)
,
P
Q
,
x
:
A
.
B
(
x
)
,
True
,
WellFnd{i}(
A
;
x
,
y
.
R
(
x
;
y
))
,
T
Lemmas
true
wf
origin
Void} 
Type
Void} Type
T
Q
x:A. B(x)
T